FDL - Step of Proof: comp_nat_ind

Step of Proof: comp_nat_ind_a

9,38

Inference at * 1 1 2 1
Iof proof for Lemma comp nat ind a:

1. P :

{k}
2.

. (

. (j < i)

P(j))

P(i)
3. s :

. (t < s)

P(t)

P(s)

by (% done % ((((((BHyp 2)

CollapseTHENM (RepD))

)

CollapseTHENM (BHyp 4))

)

CollapseTHEN (

C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))

)

Definitions t T, P Q, x:A. B(x), ,

Lemmas nat wf